ESMachineAxiom(E;T;V;M;loc;knd;val;
when;after;
sndr;Trans;Send;Choose)
== (e:E. (x.after(x,e)) = Trans(loc(e),knd(e),val(e),x.when(x,e)))
== & (e:E.
== & (islocal(knd(e))
== & ( isl(Choose(loc(e),act(knd(e)),x.when(x,e)))
== & ( & val(e) = outl(Choose(loc(e),act(knd(e)),x.when(x,e))))
== & (e:E.
== & (isrcv(knd(e))
== & ( (<lnk(knd(e)),tag(knd(e)),(val(e))>  Send
== & ( (<lnk(knd(e)),tag(knd(e)),(val(e))>  (loc(sndr(e))
== & ( (<lnk(knd(e)),tag(knd(e)),(val(e))>  ,knd(sndr(e))
== & ( (<lnk(knd(e)),tag(knd(e)),(val(e))>  ,val(sndr(e))
== & ( (<lnk(knd(e)),tag(knd(e)),(val(e))>  ,x.when(x,sndr(e))))) 

latex

---

clarification:

ESMachineAxiom(E;T;V;M;loc;knd;val;
when;after;
sndr;Trans;Send;Choose)
== (e:E. (x.after(x,e)) = Trans(loc(e),knd(e),val(e),x.when(x,e))  x:IdT(loc(e),x))
== & (e:E.
== & (islocal(knd(e))
== & ( isl(Choose(loc(e),act(knd(e)),x.when(x,e)))
== & ( & val(e) = outl(Choose(loc(e),act(knd(e)),x.when(x,e)))  V(loc(e),act(knd(e))))
== & (e:E.
== & (isrcv(knd(e))
== & ( (<lnk(knd(e)),tag(knd(e)),(val(e))>  Send
== & ( (<lnk(knd(e)),tag(knd(e)),(val(e))>  (loc(sndr(e))
== & ( (<lnk(knd(e)),tag(knd(e)),(val(e))>  ,knd(sndr(e))
== & ( (<lnk(knd(e)),tag(knd(e)),(val(e))>  ,val(sndr(e))
== & ( (<lnk(knd(e)),tag(knd(e)),(val(e))>  ,x.when(x,sndr(e)))  Msg(M))) 

latex

Definitions	x:AB(x), Id, P & Q, islocal(k), A & B, isl(x), s = t, outl(x), act(k), x:A. B(x), P  Q, b, isrcv(k), (x  l), lnk(k), <a,b>, tag(k), x.A(x), f(a), Msg(M)
FDL editor aliases	ESMachineAxiom